%context: DBC development
\emph{Bad smells} naturally arise in source code, usually as consequence of \textit{ad hoc} evolution. These smells consist in symptoms that convey likely problems, even though the program is working correctly. Examples of bad smells in object-oriented programs that motivate refactorings~\cite{refact-book} stem from classes or methods that are too long to classes using more members from other classes than its own members (Feature Envy~\cite{refact-book}). In fact, refactoring activities are often motivated by the detection of bad smells.

%DBC
On the other hand, Design-by-Contract (DBC)~\cite{dbc-meyer} establishes a method of building software by explicitly specifying what each function in a module requires in order to correctly operate, and what it provides to the caller (\emph{contracts}). They constitute a collection of assertions -- mainly invariants, pre- and post-conditions for methods -- that precisely describe what methods require and ensure with respect to client classes. Although DBC is the built-in development method for the Eiffel programming language~\cite{eiffel-book}, contracts can also be written with extensions to general-purpose languages, such as the Java Modeling Language (JML)~\cite{jml-paper} (some of its basic constructs are explained in Section~\ref{sect:jml}).

% problem
With the increasing adoption of DBC methodologies in formal software development, evidence of bad design practices can similarly be found in programs that combine actual production code with contracts. If these problems are not tackled properly, they may hinder quality benefits in DBC development, such as encapsulation, maintainability and readability (some of these problems are illustrated through an example in Section~\ref{sect:motivatingExample}).

%solution
In this paper we present a catalog of bad smells that may appear during DBC practice. 16 smells were catalogued for this paper; six of those are described in detail. Smells include symptoms like long specifications with several alternative behavior cases (\textit{Long Specs}), private fields exposed in public contracts (\textit{Open Doors}), excessive accesses to fields that represent internal data (\textit{Field Obsession}) and complex predicates that easily get very difficult to read and understand (\textit{Illogical Contracts}). 
%JML
In this work we consider JML as the language for specifying contracts~\cite{jml-dbc}; smells are described over JML constructs, although several are possible to appear in other DBC languages. Along with a name and their symptoms, we suggest actions to eliminate or minimize the effect of these smells.
% diferencial
We believe that initiatives towards a catalog of bad smells are useful to establish good design pratices in DBC.

% avaliacao
We evaluate the recurrence of the catalogued bad smells in two ways: first by describing a small study with graduate student projects; second, by counting occurrences of smells in library classes from the JML models API. This API offers classes that support specifications in JML; many of those present rather complete specifications. The API contains classes with approximately 1,600 lines of contracts. We chose one class for each category by sampling (out of 113 classes and interfaces, we picked a representative subset of six (6) files), and their analyses showed at least one type of bad smell in every exemplar -- total of seven (7) distinct smells. Despite the focus of this API is verification rather than DBC, we assume that they will be read and manipulated by developers, thus detecting the presence of bad smells is desirable.

%contributions (with overview of sections)
Discussion about related work and conclusions are included into Sections~\ref{sect:relatedWork} and~\ref{sect:conclusion}, respectively. We summarize the contributions of this paper as follows:
\begin{itemize}
	\item A catalog of DBC code smells with JML as the target contract language (Section~\ref{sect:catalogBadSmells});
	\item Evaluation of bad smells in student projects, and classes from the JML models API (Section~\ref{sect:solutionEvaluation}).
\end{itemize}